/*Z OK 调度域 */

/*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * SPDX-License-Identifier: GPL-2.0-only
 */

#include <object/structures.h>
#include <model/statedata.h>
/*Z 可配置的调度域。每个域有固定的调度周期，每个线程属于一个域，只有在域活跃时线程才能执行。sel4test不用此文件，用projects/sel4test/domain_schedule.c */
/* Default schedule. */
const dschedule_t ksDomSchedule[] = {
    { .domain = 0, .length = 1 },
};
/*Z 调度域数量 */
const word_t ksDomScheduleLength = sizeof(ksDomSchedule) / sizeof(dschedule_t);

